#include<iostream>
#include<fstream>
#include<stdlib.h>
#include<set>
#include<list>
#include<algorithm>


using namespace std;
#define N 7777
typedef struct Node
{
    int n;
    struct Node* next;
}node, *pNode;


int v_num, s_num;
int devide(list<int> l[]);
int Judge(list<int> l[]);
void findL(list<int> l[], list<int> l1[], list<int> l2[]);
int ss(list<int> l[]);
int deleteS(list<int> l[], int e);
void repeatS(list<int> l[]);


void get_info(int& var_num, int& son_num, pNode* p)
{
	char buffer[144];
    pNode p1 = NULL, p0 = NULL;
    int t = 0, i = 0;
    char c;
	var_num = 0, son_num = 0;
	ifstream infile;
	infile.open("test5.dat");
	if(!infile.is_open()) return;

    infile.seekg(23);  // 定位到某个位置
    infile >> var_num;
    infile >> son_num;

	while(!infile.eof())	// 读取数字
	{
		infile >> t;
        p[i] = (pNode)malloc(sizeof(node));
        p[i]->next = NULL;
        p0 = p[i];
        while(t != 0)
        {
            p1 = (pNode)malloc(sizeof(node));
            p1->next = NULL;
            p1->n = t;
            p0->next = p1;
            p0 = p1;
            infile >> t;
        }
        p[i] = p[i]->next;  // 去掉头节点的影响
        i++;
	}
}


int main()
{
    list<int> l[N];
    pNode p[N], p0;
    int isok = 0;
    get_info(v_num, s_num, p);
    for(int i = 0; i < s_num; i++)
    {
        p0 = p[i];
        while(p0)
        {
            l[i].push_back(p0->n);
            p0 = p0->next;
        }
        // cout << endl;
    }
    repeatS(l);
    isok = devide(l);
    cout << isok << endl;
    return 0;
}


int devide(list<int> l[])  // 分裂规则和单子句规则综合
{
    int size = 0;
    /*
    for(int j = 0; j < s_num; j++)
    {
        if(!l[j].empty()) size++;
    }
    if(size <= 50)
    {
        cout << "l:" << endl;
        for(int i = 0; i < s_num; i++)
        {
            list<int>::iterator itr1 = l[i].begin();
            while(itr1 != l[i].end())
            {
                cout << *itr1 << " ";
                itr1++;
            }
            if(!l[i].empty()) cout << endl;
        }
        cout << "result: " << Judge(l) << endl;
        cout << "--------------------------" << endl << endl;
    }
    */
    list<int> l1[N], l2[N];
    int key1 = 1, key2 = 1;
    key1 = Judge(l);
    if(key1 == -1) 
    {
        // cout << "end!";
        return 0;  // 先判断一下
    }
    else if(key1 == 0) return 1;
    key2 = ss(l);
    if(key2 == -1) return 0;
    else if(key2 == 0) return 1;
    // 分裂规则
    findL(l, l1, l2);
    /*
    if(size <= 50)
    {
        cout << "l1:" << endl;
        for(int i = 0; i < s_num; i++)
        {
            list<int>::iterator itr1 = l1[i].begin();
            while(itr1 != l1[i].end())
            {
                cout << *itr1 << " ";
                itr1++;
            }
            if(!l[i].empty()) cout << endl;
        }
        cout << "result: " << Judge(l1) << endl;
        cout << "--------------------------" << endl << endl;
    }
    if(size <= 50)
    {
        cout << "l2:" << endl;
        for(int i = 0; i < s_num; i++)
        {
            list<int>::iterator itr1 = l2[i].begin();
            while(itr1 != l2[i].end())
            {
                cout << *itr1 << " ";
                itr1++;
            }
            if(!l[i].empty()) cout << endl;
        }
        cout << "result: " << Judge(l2) << endl;
        cout << "--------------------------" << endl << endl;
    }
    */
    l->clear();
    // cout << "size: " << l->size() << endl;
    return (devide(l1) || devide(l2));
}


int Judge(list<int> l[])  // 统计子句数目，变量数目，   需要讨论
{
    int key = 0, count = 0;
    int e1 = 0, e2 = 0;
    for(int i = 0; i < s_num; i++)
    {
        if(!l[i].empty()) count++;
        if(l[i].size() == 1)
        {
            e1 = l[i].front();
            // cout << "e1:" << e1 << endl; 
            
            for(int j = i+1; j < s_num; j++)
            {
                if(l[j].size() == 1)
                {
                    e2 = -1*l[j].front();
                    // cout << "e2:" << e2 << endl;
                    if(e1 == e2)
                    {
                        key = 1;
                        i = s_num;
                        break;
                    }
                }
            }
            
        }
    }
    if(key) return -1;
    else if(count == 0) return 0;
    else return 1;
}


void findL(list<int> l[], list<int> l1[], list<int> l2[])  // 分裂规则
{
    int e = 0;
    int t1 = 0, t2 = 0;

    for(int i = 0; i < s_num; i++)
    {
        if(!l[i].empty())
        {
            e = l[i].front();  // 随便找一个分裂标准
            break;
        }
    }
    // cout << "e:" << e << endl;
    for(int i = 0; i < s_num; i++)
    {
        list<int>::iterator itr1;
        list<int>::iterator itr2;
        if(!l[i].empty())
        {
            itr1 = find(l[i].begin(), l[i].end(), e);
            itr2 = find(l[i].begin(), l[i].end(), -1*e);
            if(itr1 != l[i].end())
            {
                l1[t1] = l[i];
                l1[t1].remove(e);
                /*
                cout << "e: " << e << endl;
                for(itr1 = l[t1].begin(); itr1 != l[t1].end(); itr1++)
                {
                    cout << *itr1 << " ";
                }
                cout << endl << "-----------------------" << endl;
                */
                t1++;
            }
            else if(itr2 != l[i].end())
            {
                l2[t2] = l[i];  // 非p
                l2[t2].remove(-1*e);
                t2++;
            }
            else
            {
                l1[t1] = l[i];  // 其他
                t1++;
                l2[t2] = l[i];
                t2++;
            }
        }
    }
}


int ss(list<int> l[])  //单子句规则 - 找到所需的
{
    int key = 1;
    for(int i = 0; i < s_num; i++)
    {
        if(l[i].size() == 1)
        {
            deleteS(l, l[i].front());
            /*
            for(int i = 0; i < s_num; i++)
            {
                list<int>::iterator itr1 = l[i].begin();
                while(itr1 != l[i].end())
                {
                    cout << *itr1 << " ";
                    itr1++;
                }
                cout << endl;
            }
		    cout << "-----------------------------------------" << endl;
            */
        }
        key = Judge(l);
        if(key == -1) return -1;
        else if(key == 0) return 0;
          
    }
    return 1;
}


int deleteS(list<int> l[], int e)  // 单子句规则
{
    int key1 = 0, key2 = 0;
    list<int>::iterator itr1;
    list<int>::iterator itr2;
    for(int i = 0; i < s_num; i++)
    {
        itr1 = l[i].begin();
        itr2 = l[i].begin();
        itr1 = find(l[i].begin(), l[i].end(), e);
        itr2 = find(l[i].begin(), l[i].end(), -1*e);
        if(itr1 != l[i].end())  // 相同
        {
            if(l[i].size() == 1) key1 = 1;
            l[i].clear();
        }
        else if(itr2 != l[i].end())  // 相反
        {
            if(l[i].size() == 1) key2 = 1;
            l[i].remove(-1*e);
        }
        if(key1 && key2) return -1;
    }
    return false;
}


void repeatS(list<int> l[])  // 删除所有重言式
{
    list<int>::iterator itr1;
    for(int i = 0; i < s_num; i++)
    {
        if(!l[i].empty())
        {
            int e;
            itr1 = l[i].begin();
            list<int>::iterator itr;
            for(itr = l[i].begin(); itr != l[i].end(); itr++)
            {
               // cout << *itr << endl;
                e = *itr;
                itr1 = find(l[i].begin(), l[i].end(), -1*e);  // 出现重言式，即删除子句
                if(itr1!=l[i].end()) 
				{
					l[i].clear();
					break;
				}
            }
        }
    }
}
